A1,A2:Type, B1:(A1Type), B2:(A2Type).
strong-subtype(A1; A2)
 (a:A1. subtype_rel(B1(a); B2(a)))
 subtype_rel(fpf(A1; a.B1(a)); fpf(A2; a.B2(a))) 

latex

Definitions	l[i], , A  B, A, ||as||, P  Q, guard(T), P  Q, P  Q, False, subtype(S; T), suptype(S; T), (x  l), strong-subtype(A; B), prop{i:l}, x:A. B(x), P  Q, A c B, fpf(A; a.B(a)), x:A. B(x), x. t(x), x(s), t  T
Lemmas	fpf wf, l member wf, nil member, cons member, select wf, length wf1